A:Type, eq:EqDecider(A), B:(AType), f:a:A fp B(a), x:A, v:B(x). x  dom(f)  f || x : v 

latex

Definitions	t  T, x(s), x:A. B(x), x. t(x), Top, a:A fp B(a), x  dom(f), b, False, P  Q, A, P & Q, P  Q, x : v, Prop, f(x), f || g, EqDecider(T)
Lemmas	not wf, fpf wf, deq wf, fpf-single wf, top wf, fpf-single-dom, assert wf, fpf-dom wf, fpf-trivial-subtype-top